/* Benchmarks for the PionterC verifier. */

// clear a list

struct list 
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @               ({{l}} && list(l->next))
  @ in  list(l)
  @ end
  @*/
void ClearList(struct list * l)
{
  struct list *p;
  p=l;
  while(p!=null) /*@{{p, l}} && list(l->next) */  // <=== note that this is a short circuite.
  {
    l = l->next;
    free(p);
    p=l;
  }
  return;
}
/*@ list(l)*/ // <=== empty list.
